The Book of Shen 4th Edition

Author's Note

This is an online version of the Book of Shen, 4th edition available from Amazon. If you are reading TBoS to understand Shen, first click on 'How to Read this Book' in the table of contents.

Programs by section and chapter

3.2 3.3 3.4 3.5 3.6 3.7 4.3 4.4 4.5 5.4 6.4 6.5 7.1 8.1 8.3 8.4 8.5 8.6 8.7 9.1 9.2 10.4 10.5 11.2 12.2 12.4 13.2 13.3 13.4 13.5 13.6 13.7 13.8 13.9 14.4 14.5 14.6 14.7 15.1 15.2 15.7 17.5 17.6 17.7 18.6 19.1 19.2 19.4 19.5 19.6 19.8 20.3 20.4 20.6 20.7 20.8 20.9 21.1 21.3 21.4 21.5 22.2 22.3 23.2 23.3 23.4.1 23.4.2 24.3 24.4 24.5 24.6 24.7 24.8 24.9 25.3 25.6 25.7 27.19 28.3

Index

Updates to the Language Standard

Brought in with version 34: Assert and Retract in Shen Prolog

Table of Contents

Dedication iii

How to Read this Book xi
A Conceptual Dependency Table xii
Preface to the Fourth Edition xiii
Acknowledgements xiv

Chapter 1 Beginnings 1

1.1 Declarative Programming 1
1.2 Mathematical Foundations 2
1.3 The American Experience 7
1.4 The British Experience 10
1.5 The Forerunners of Shen: SEQUEL 13
1.6 The Forerunners of Shen: Qi 14
1.7 Shen 16

Part I The Core Language

Chapter 2 Starting Shen 20

2.1 Starting Up 20
2.2 Applying Functions 21
2.3 Repeating Evaluations 22
2.4 Strict and Non-Strict Evaluation 23
2.5 Boolean Operations 24
2.6 Defining New Functions 25
2.7 Equations and Priority Rewrite Systems 27
2.8 A Bible Studies Program 29

Chapter 3 Recursion 34

3.1 Of Numbers 34
3.2 Recursion and the Factorial Function 37
3.3 Forms of Recursion 38
3.4 Tracing Function Calls 41
3.5 Guards 41
3.6 Counting Change 44
3.7 Non-terminating Functions 45

Chapter 4 Lists 49

4.1 Representing Lists in Shen 49
4.2 Building Lists with cons 50
4.3 hd and tl Access List Components 52
4.4 Local Assignments 56>
4.5 Goldbach’s Conjecture Revisited 57

Chapter 5 Strings 61

5.1 Strings and Symbols 61
5.2 Building Strings with make-string 64
5.3 Coercing Strings to Lists 65
5.4 Programming with Strings 66

Chapter 6 Higher Order Functions 70

6.1 Higher Order Functions 70
6.2 Abstractions, Currying and Partial Applications 71
6.3 fn and Abstractions 73
6.4 Overapplications 73
6.5 Programming with Higher Order Functions 74

Chapter 7 Assignments 81

7.1 Simple Assignments 81
7.2 Destructive Operations 82

Chapter 8 Vectors 85

8.1 Vectors 85
8.2 Lists and Vectors 86
8.3 Handling Vectors 88
8.4 Timing Operations 89
8.5 Hash Tables 91
8.6 Property Vectors and Semantic Nets 93
8.7 Native Vectors and Print Vectors 95

Chapter 9 I/O 99

9.1 Streams 99
9.2 Print Functions 100
9.3 Reading Input 102
9.4 Reading from a String 104
9.5 String Searching Text Files 105

Chapter 10 Macros and Packages 108

10.1 Macros 108
10.2 Changing the Order of Evaluation 111
10.3 Defining our own Notation 111
10.4 Packages 112
10.5 Packages that Use Packages 115
10.6 The Null Package and Macros 116
10.7 DSLs, Macros and Packages 118
10.8 Macro Management 119
10.9 Macroexpansion and Unpackaging 120
10.9 Working Inside a Package 121

Chapter 11 Exceptions and Continuations 123

11.1 Exceptions 123
11.2 Continuations 125

Chapter 12 Non-determinism 129

12.1 Non-deterministic Algorithms 129
12.2 Depth First Search 129
12.3 Recursive Descent Parsing 132
12.4 A Recursive Descent Parser in Shen 136

Chapter 13 Shen YACC 142

13.1 A Short History of Shen YACC 142
13.2 Programming in Shen YACC 143
13.3 The Empty Expansion and Guards 145
13.4 Non-terminals and Semantic Actions 146
13.5 Handling Lists in Shen YACC 148
13.6 Efficient Parsing 149
13.7 Consuming the Input 150
13.8 Limited Backtracking 151
13.9 Left Recursion 152

Chapter 14 Lambda Calculus* 156

14.1 The Notation of the Lambda Calculus 156
14.2 Reasoning with the Lambda Calculus 158
14.3 The Church-Rosser Theorems 160
14.4 Conditionals 162
14.5 Weak Head Normal Form 164
14.6 Tuples 166
14.7 Numbers 167
14.8 Recursion and the Y-combinator 168

Chapter 15 Kλ* 171

15.1 From Lambda Calculus to Kλ 171
15.2 Character Streams and Byte Streams 174
15.3 Foreign Functions 177
15.4 Manipulating Kλ 177
15.4 From Shen to Kλ via an Extended λ Calculus 178
15.5 Compiling Out Choicepoints 182
15.6 The Triple Stack Method 183
15.7 Factorising Kλ 186

15.8 Factorisation at Work 191

Chapter 16 Writing Good Programs 194

Part II Working with Types

Chapter 17 Types 199

17.1 Types and Type Security 199
17.2 Modifying the Read-Evaluate-Print Loop 200
17.3 Lists, Vectors and Tuples 201
17.4 Lazy Types 203
17.5 The Small Arrow Type 204
17.6 Polymorphic Types 206
17.7 Equality Types 208
17.8 Stream Types 209
17.9 Types and Optimisation 210
17.10 Changing the Type of a Function 211
17.11 The Limits of Inbuilt Types 211

Chapter 18 Sequent Calculus 214

18.1 Sequent Calculus and Computer Science 214
18.2 Introducing Sequent Calculus 215
18.3 Propositional Calculus 217
18.4 First Order Logic (FOL) 221
18.5 Proof Trees and Goal Stacks 224
18.6 Implementing a Stack Based System: Proplog 225
18.7 Soundness and Completeness 228

Chapter 19 Concrete Types 231

19.1 Enumeration Types 231
19.2 Left and Right Rules 234
19.3 Handling Global Variables 236
19.4 Recursive Types (I): the Lambda Calculus 238
19.5 Recursive Types (II): Proplog 240
19.6 Dynamic Type Checking 241
19.7 Analytic and Synthetic Rules 244
19.8 Defining Polyadic Types 245

Chapter 20 Proof and Control 250

20.1 Controlling Timeout 250
20.2 Using spy to Trace Type Checking 251
20.3 Using Cuts 254
20.4 Type Annotations 255
20.5 preclude and include 256
20.6 Ordering Rules: Subtypes 257
20.7 Controlling Infinite Loops: Mode Declarations 260
20.8 Dependent Types 263
20.9 Creating a Tabula Rasa 265

Chapter 21 Abstract and Algebraic Datatypes 266

21.1 Concrete and Abstract Datatypes 266
21.2 Abstract Datatypes in Sequent Calculus 268
21.3 Proofs in a Hilbert System 269
21.4 Algebraic Simplification 274
21.5 Shen and ML 277

Chapter 22 Typed Shen YACC 284

22.1 The Big Arrow Type 284
22.2 Parsing Bytes to Numbers 285
22.3 Montague Grammars 288
22.4 YACC Structures 293
22.5 Abstract Operations* 294
22.6 The Concrete Implementation* 297
22.7 The Compilation of YACC Rules* 298

Chapter 23 A Model Checker 305

23.1 An Introduction to Model Theory 305
22.2 Implementing a Model Checker 307
23.3 Dealing with Infinity 309
23.4 Super Quantification 312
23.5 Proof and Computability 314

Chapter 24 An Interpreter for Kλ 316

24.1 Formal Semantics 316
24.2 The Environment Model of Evaluation 317
24.3 The Basic SECD Machine 319
24.4 Computing with the SECD Machine 321
24.5 Adding δ Rules to the SECD Machine 327
24.6 Adding Lazy Evaluation to the SECD Machine 329
24.7 Adding Global Definitions to the SECD Machine 331
24.8 Quotation and Lexical Scope 333
24.9 List Processing in the SECD Machine 340

Chapter 25 Shen Prolog 345

25.1 A Short History of Prolog 345
25.2 Horn Clause Logic 346
25.3 Unification 347
25.4 Programming in Horn Clause Logic 353
25.5 Programming in Prolog 355
25.6 Shen Prolog 357
25.7 Implementing a Horn Clause Interpreter 363

Chapter 26 Compiling Sequent Calculus* 369

26.1 The Anatomy of a Sequent Calculus Rule 369
26.2 Sequent Calculus as a Source Language 370
26.3 Enriched Horn Clause Logic as an Object Language 374
26.4 Two Models for Compiling Sequent Calculus 374
26.5 Naïve Goal Oriented Compilation in Shen 376
26.6 Refining Goal Oriented Compilation 380

Chapter 27 Compiling Prolog* 383

27.1 The Binding Vector 383
27.2 The Continuation 384
27.3 Eager vs. Lazy Dereferencing 384
27.4 Left Linear Horn Clauses 385
27.5 Implementing Unification 385
27.6 Coping with Exponential Code 387
27.7 The Twin Stack Method 388
27.8 Compiling the Head of the Clause 389
27.9 The Variable Case 391
27.10 The Negative Atom Case 391
27.11 The Negative Cons Case 391
27.12 The Positive Atom Case 392
27.13 The Positive Cons Case 392
27.14 Garbage Collection 395
27.15 Constructing the Continuation 395
27.16 Constructing a Horn Clause Procedure 398
27.17 Implementing the Cut 399
27.18 Implementing findall 403
27.18 Optimising Shen Prolog Programs 404
27.19 Shen Prolog Performance 406

Chapter 28 The Semantics of L* 410

28.1 An Overview of Our Approach 410
28.2 An Operational Semantics for L 412
28.3 An Interpreter for L 414
28.4 Compilation to Kλ and Semantics 415

Chapter 29 System S* 423

29.1 Type Checking Applications 423
29.2 Type Checking Abstractions 424
29.3 Polymorphic Functions 425
29.4 Special Forms 426
29.5 Recursion, Cases, Patterns and Guards 427
29.6 Global Variables 430

Chapter 30 Type Safety* 432

30.1 The Correctness of S 432
30.2 T 438
30.3 Procedure T* 442
30.4 The Equivalence of T and T* 448
30.5 T* in Shen 451

Appendices

Appendix A System Functions and their Types in Shen 459
Appendix B The Syntax of Shen 475
Appendix C The Next Lisp: Back to the Future 478

Bibliography 485
Index of System Functions Used in this Book 498
Index 500